YES 22.252
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (\vv1 ->
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
) (zip xs (enumFrom 0)) |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
Lambda Reductions:
The following Lambda expression
\vv1→
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices0 | p vv1 | =
case | vv1 of | | (x,i) | → if p x then i : [] else [] |
| _ | → [] |
|
The following Lambda expression
\ab→(a,b)
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule List
| ((elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = |
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
|
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
Case Reductions:
The following Case expression
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices00 | p (x,i) | = if p x then i : [] else [] |
findIndices00 | p _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule List
| ((elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | if p x then i : [] else [] |
findIndices00 | p _ | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
If Reductions:
The following If expression
if p x then i : [] else []
is transformed to
findIndices000 | i True | = i : [] |
findIndices000 | i False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p _ | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : vx) | = | Just a |
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule List
| ((elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : vx) | = | Just a |
|
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule List
| (elemIndex :: Ratio Int -> [Ratio Int] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero))) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : vx) | = | Just a |
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe1(wz217, Succ(wz2180), Zero, wz220, :(wz2210, wz2211), wz222) → new_listToMaybe(wz220, wz2210, wz2211, new_primPlusNat(wz222), new_primPlusNat(wz222))
new_listToMaybe2(wz243, wz220, wz22101, wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Zero), Pos(wz221010)), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe1(wz217, Succ(wz2180), Succ(wz2190), wz220, wz221, wz222) → new_listToMaybe1(wz217, wz2180, wz2190, wz220, wz221, wz222)
new_listToMaybe0(wz217, wz220, :(wz2210, wz2211), wz222) → new_listToMaybe(wz220, wz2210, wz2211, new_primPlusNat(wz222), new_primPlusNat(wz222))
new_listToMaybe(wz220, :%(Neg(Succ(wz2210000)), wz22101), wz2211, wz244, wz243) → new_listToMaybe2(wz243, wz220, wz22101, wz2211)
new_listToMaybe(wz220, :%(Neg(Zero), wz22101), wz2211, wz244, wz243) → new_listToMaybe3(wz243, wz220, wz22101, wz2211)
new_listToMaybe3(wz243, wz220, Neg(Zero), wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Zero), Neg(Succ(wz2210100))), wz2211, wz244, wz243) → new_listToMaybe1(wz243, wz220, wz2210100, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Succ(wz2210000)), wz22101), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe1(wz217, Zero, Succ(wz2190), wz220, wz221, wz222) → new_listToMaybe0(wz217, wz220, wz221, wz222)
new_listToMaybe3(wz243, wz220, Neg(Succ(wz2210100)), wz2211) → new_listToMaybe1(wz243, wz220, wz2210100, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Zero), Neg(Zero)), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe3(wz243, wz220, Pos(wz221010), wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The TRS R consists of the following rules:
new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_listToMaybe(wz220, :%(Pos(Zero), Neg(Succ(wz2210100))), wz2211, wz244, wz243) → new_listToMaybe1(wz243, wz220, wz2210100, wz220, wz2211, wz243)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 1 >= 4, 3 >= 5, 5 >= 6
- new_listToMaybe(wz220, :%(Neg(Succ(wz2210000)), wz22101), wz2211, wz244, wz243) → new_listToMaybe2(wz243, wz220, wz22101, wz2211)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 3 >= 4
- new_listToMaybe0(wz217, wz220, :(wz2210, wz2211), wz222) → new_listToMaybe(wz220, wz2210, wz2211, new_primPlusNat(wz222), new_primPlusNat(wz222))
The graph contains the following edges 2 >= 1, 3 > 2, 3 > 3
- new_listToMaybe1(wz217, Succ(wz2180), Zero, wz220, :(wz2210, wz2211), wz222) → new_listToMaybe(wz220, wz2210, wz2211, new_primPlusNat(wz222), new_primPlusNat(wz222))
The graph contains the following edges 4 >= 1, 5 > 2, 5 > 3
- new_listToMaybe1(wz217, Succ(wz2180), Succ(wz2190), wz220, wz221, wz222) → new_listToMaybe1(wz217, wz2180, wz2190, wz220, wz221, wz222)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_listToMaybe3(wz243, wz220, Neg(Succ(wz2210100)), wz2211) → new_listToMaybe1(wz243, wz220, wz2210100, wz220, wz2211, wz243)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 2 >= 4, 4 >= 5, 1 >= 6
- new_listToMaybe1(wz217, Zero, Succ(wz2190), wz220, wz221, wz222) → new_listToMaybe0(wz217, wz220, wz221, wz222)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4
- new_listToMaybe(wz220, :%(Neg(Zero), wz22101), wz2211, wz244, wz243) → new_listToMaybe3(wz243, wz220, wz22101, wz2211)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 3 >= 4
- new_listToMaybe2(wz243, wz220, wz22101, wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe(wz220, :%(Pos(Zero), Pos(wz221010)), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe(wz220, :%(Pos(Succ(wz2210000)), wz22101), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe(wz220, :%(Pos(Zero), Neg(Zero)), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe3(wz243, wz220, Neg(Zero), wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe3(wz243, wz220, Pos(wz221010), wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe6(wz210, Succ(wz2110), Zero, wz213, :(wz2140, wz2141), wz215) → new_listToMaybe4(wz213, wz2140, wz2141, new_primPlusNat(wz215), new_primPlusNat(wz215))
new_listToMaybe4(wz213, :%(Neg(Succ(wz2140000)), wz21401), wz2141, wz242, wz241) → new_listToMaybe7(wz241, wz213, wz21401, wz2141)
new_listToMaybe5(wz210, wz213, :(wz2140, wz2141), wz215) → new_listToMaybe4(wz213, wz2140, wz2141, new_primPlusNat(wz215), new_primPlusNat(wz215))
new_listToMaybe8(wz241, wz213, Pos(Succ(wz2140100)), wz2141) → new_listToMaybe6(wz241, wz213, wz2140100, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Pos(Zero), Pos(Succ(wz2140100))), wz2141, wz242, wz241) → new_listToMaybe6(wz241, wz213, wz2140100, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Neg(Zero), wz21401), wz2141, wz242, wz241) → new_listToMaybe8(wz241, wz213, wz21401, wz2141)
new_listToMaybe8(wz241, wz213, Pos(Zero), wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe8(wz241, wz213, Neg(wz214010), wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Pos(Zero), Pos(Zero)), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe6(wz210, Succ(wz2110), Succ(wz2120), wz213, wz214, wz215) → new_listToMaybe6(wz210, wz2110, wz2120, wz213, wz214, wz215)
new_listToMaybe4(wz213, :%(Pos(Zero), Neg(wz214010)), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe7(wz241, wz213, wz21401, wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Pos(Succ(wz2140000)), wz21401), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe6(wz210, Zero, Succ(wz2120), wz213, wz214, wz215) → new_listToMaybe5(wz210, wz213, wz214, wz215)
The TRS R consists of the following rules:
new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_listToMaybe4(wz213, :%(Pos(Zero), Pos(Succ(wz2140100))), wz2141, wz242, wz241) → new_listToMaybe6(wz241, wz213, wz2140100, wz213, wz2141, wz241)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 1 >= 4, 3 >= 5, 5 >= 6
- new_listToMaybe7(wz241, wz213, wz21401, wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe4(wz213, :%(Neg(Zero), wz21401), wz2141, wz242, wz241) → new_listToMaybe8(wz241, wz213, wz21401, wz2141)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 3 >= 4
- new_listToMaybe4(wz213, :%(Neg(Succ(wz2140000)), wz21401), wz2141, wz242, wz241) → new_listToMaybe7(wz241, wz213, wz21401, wz2141)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 3 >= 4
- new_listToMaybe6(wz210, Succ(wz2110), Succ(wz2120), wz213, wz214, wz215) → new_listToMaybe6(wz210, wz2110, wz2120, wz213, wz214, wz215)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_listToMaybe8(wz241, wz213, Pos(Succ(wz2140100)), wz2141) → new_listToMaybe6(wz241, wz213, wz2140100, wz213, wz2141, wz241)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 2 >= 4, 4 >= 5, 1 >= 6
- new_listToMaybe6(wz210, Succ(wz2110), Zero, wz213, :(wz2140, wz2141), wz215) → new_listToMaybe4(wz213, wz2140, wz2141, new_primPlusNat(wz215), new_primPlusNat(wz215))
The graph contains the following edges 4 >= 1, 5 > 2, 5 > 3
- new_listToMaybe5(wz210, wz213, :(wz2140, wz2141), wz215) → new_listToMaybe4(wz213, wz2140, wz2141, new_primPlusNat(wz215), new_primPlusNat(wz215))
The graph contains the following edges 2 >= 1, 3 > 2, 3 > 3
- new_listToMaybe6(wz210, Zero, Succ(wz2120), wz213, wz214, wz215) → new_listToMaybe5(wz210, wz213, wz214, wz215)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4
- new_listToMaybe4(wz213, :%(Pos(Zero), Pos(Zero)), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe4(wz213, :%(Pos(Zero), Neg(wz214010)), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe4(wz213, :%(Pos(Succ(wz2140000)), wz21401), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe8(wz241, wz213, Pos(Zero), wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe8(wz241, wz213, Neg(wz214010), wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe12(wz62, Neg(Succ(wz3100)), Pos(wz411010), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe12(wz62, Neg(Zero), Neg(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe9(Neg(Zero), :%(Pos(Zero), Pos(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe9(Pos(Zero), :%(Pos(Zero), Neg(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe9(Neg(Succ(wz3100)), :%(Pos(Zero), Pos(wz411010)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(wz31, :%(Pos(Succ(wz4110000)), wz41101), :(wz41110, wz41111), wz62, wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
new_listToMaybe9(Pos(Succ(wz3100)), :%(Pos(Zero), Neg(wz411010)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(wz31, :%(Neg(Zero), wz41101), wz4111, wz62, wz63) → new_listToMaybe12(wz62, wz31, wz41101, wz4111, wz63)
new_listToMaybe9(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Zero)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe10(wz62, wz31, :(wz41110, wz41111), wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
new_listToMaybe12(wz62, Pos(Zero), Pos(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe12(wz62, Pos(Succ(wz3100)), Neg(wz411010), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(Pos(Zero), :%(Pos(Zero), Pos(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe11(wz62, wz31, wz41101, :(wz41110, wz41111), wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
new_listToMaybe9(Neg(Zero), :%(Pos(Zero), Neg(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe12(wz62, Neg(Succ(wz3100)), Neg(Zero), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe12(wz62, Pos(Zero), Neg(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe9(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Zero)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe12(wz62, Neg(Zero), Pos(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe12(wz62, Pos(Succ(wz3100)), Pos(Zero), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(wz31, :%(Neg(Succ(wz4110000)), wz41101), wz4111, wz62, wz63) → new_listToMaybe11(wz62, wz31, wz41101, wz4111, wz63)
The TRS R consists of the following rules:
new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_listToMaybe10(wz62, wz31, :(wz41110, wz41111), wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
The graph contains the following edges 2 >= 1, 3 > 2, 3 > 3
- new_listToMaybe9(wz31, :%(Neg(Zero), wz41101), wz4111, wz62, wz63) → new_listToMaybe12(wz62, wz31, wz41101, wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 2 > 3, 3 >= 4, 5 >= 5
- new_listToMaybe9(wz31, :%(Pos(Succ(wz4110000)), wz41101), :(wz41110, wz41111), wz62, wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3
- new_listToMaybe11(wz62, wz31, wz41101, :(wz41110, wz41111), wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
The graph contains the following edges 2 >= 1, 4 > 2, 4 > 3
- new_listToMaybe9(wz31, :%(Neg(Succ(wz4110000)), wz41101), wz4111, wz62, wz63) → new_listToMaybe11(wz62, wz31, wz41101, wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 2 > 3, 3 >= 4, 5 >= 5
- new_listToMaybe9(Neg(Zero), :%(Pos(Zero), Pos(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Pos(Zero), :%(Pos(Zero), Neg(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 2 > 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Neg(Succ(wz3100)), :%(Pos(Zero), Pos(wz411010)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Pos(Succ(wz3100)), :%(Pos(Zero), Neg(wz411010)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Zero)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Pos(Zero), :%(Pos(Zero), Pos(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 2 > 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Neg(Zero), :%(Pos(Zero), Neg(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe9(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Zero)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 4 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Neg(Succ(wz3100)), Pos(wz411010), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Neg(Zero), Neg(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Pos(Zero), Pos(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Pos(Succ(wz3100)), Neg(wz411010), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Neg(Succ(wz3100)), Neg(Zero), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Pos(Zero), Neg(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Neg(Zero), Pos(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_listToMaybe12(wz62, Pos(Succ(wz3100)), Pos(Zero), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe15(wz272, Zero, Zero, Pos(Zero), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Zero), wz278, wz272)
new_listToMaybe14(wz167, wz168, wz169, wz170, :(wz1710, wz1711), wz172) → new_listToMaybe13(wz170, wz168, wz1710, wz1711, new_primPlusNat(wz172), new_primPlusNat(wz172))
new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe17(wz272, wz27500, wz27600, wz277, wz27500, wz278)
new_listToMaybe18(wz311, Succ(wz3120), Succ(wz3130), wz314, wz315, wz316) → new_listToMaybe18(wz311, wz3120, wz3130, wz314, wz315, wz316)
new_listToMaybe15(wz272, Zero, Zero, Pos(Zero), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Zero), wz278, wz272)
new_listToMaybe13(wz170, wz168, :%(Neg(Zero), wz17101), wz1711, wz188, wz187) → new_listToMaybe14(wz187, wz168, wz17101, wz170, wz1711, wz187)
new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Pos(Zero), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Succ(wz27500)), wz278, wz272)
new_listToMaybe18(wz311, Zero, Succ(wz3130), wz314, wz315, wz316) → new_listToMaybe16(wz311, wz314, Neg(Succ(wz315)), wz316, wz311)
new_listToMaybe18(wz311, Succ(wz3120), Zero, wz314, wz315, wz316) → new_listToMaybe16(wz311, wz314, Neg(Succ(wz315)), wz316, wz311)
new_listToMaybe13(wz170, wz168, :%(Pos(wz171000), wz17101), wz1711, wz188, wz187) → new_listToMaybe14(wz187, wz168, wz17101, wz170, wz1711, wz187)
new_listToMaybe15(wz272, Succ(wz2730), Zero, wz275, wz276, wz277, wz278) → new_listToMaybe14(wz272, wz275, wz276, wz277, wz278, wz272)
new_listToMaybe15(wz272, Zero, Succ(wz2740), wz275, wz276, wz277, wz278) → new_listToMaybe14(wz272, wz275, wz276, wz277, wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Zero), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Zero), wz278, wz272)
new_listToMaybe13(wz170, wz168, :%(Neg(Succ(wz1710000)), wz17101), wz1711, wz188, wz187) → new_listToMaybe15(wz187, wz170, wz1710000, wz168, wz17101, wz170, wz1711)
new_listToMaybe15(wz272, Zero, Zero, Neg(Zero), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Zero), wz278, wz272)
new_listToMaybe17(wz304, Succ(wz3050), Zero, wz307, wz308, wz309) → new_listToMaybe16(wz304, wz307, Pos(Succ(wz308)), wz309, wz304)
new_listToMaybe17(wz304, Zero, Succ(wz3060), wz307, wz308, wz309) → new_listToMaybe16(wz304, wz307, Pos(Succ(wz308)), wz309, wz304)
new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Neg(wz2760), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Succ(wz27500)), wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Neg(Zero), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Succ(wz27500)), wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Pos(wz2760), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Succ(wz27500)), wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe18(wz272, wz27500, wz27600, wz277, wz27500, wz278)
new_listToMaybe16(wz167, wz170, wz168, :(wz1710, wz1711), wz172) → new_listToMaybe13(wz170, wz168, wz1710, wz1711, new_primPlusNat(wz172), new_primPlusNat(wz172))
new_listToMaybe15(wz272, Succ(wz2730), Succ(wz2740), wz275, wz276, wz277, wz278) → new_listToMaybe15(wz272, wz2730, wz2740, wz275, wz276, wz277, wz278)
new_listToMaybe17(wz304, Succ(wz3050), Succ(wz3060), wz307, wz308, wz309) → new_listToMaybe17(wz304, wz3050, wz3060, wz307, wz308, wz309)
The TRS R consists of the following rules:
new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_listToMaybe16(wz167, wz170, wz168, :(wz1710, wz1711), wz172) → new_listToMaybe13(wz170, wz168, wz1710, wz1711, new_primPlusNat(wz172), new_primPlusNat(wz172))
The graph contains the following edges 2 >= 1, 3 >= 2, 4 > 3, 4 > 4
- new_listToMaybe13(wz170, wz168, :%(Neg(Succ(wz1710000)), wz17101), wz1711, wz188, wz187) → new_listToMaybe15(wz187, wz170, wz1710000, wz168, wz17101, wz170, wz1711)
The graph contains the following edges 6 >= 1, 1 >= 2, 3 > 3, 2 >= 4, 3 > 5, 1 >= 6, 4 >= 7
- new_listToMaybe15(wz272, Succ(wz2730), Succ(wz2740), wz275, wz276, wz277, wz278) → new_listToMaybe15(wz272, wz2730, wz2740, wz275, wz276, wz277, wz278)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
- new_listToMaybe18(wz311, Succ(wz3120), Succ(wz3130), wz314, wz315, wz316) → new_listToMaybe18(wz311, wz3120, wz3130, wz314, wz315, wz316)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe18(wz272, wz27500, wz27600, wz277, wz27500, wz278)
The graph contains the following edges 1 >= 1, 4 > 2, 5 > 3, 6 >= 4, 4 > 5, 7 >= 6
- new_listToMaybe14(wz167, wz168, wz169, wz170, :(wz1710, wz1711), wz172) → new_listToMaybe13(wz170, wz168, wz1710, wz1711, new_primPlusNat(wz172), new_primPlusNat(wz172))
The graph contains the following edges 4 >= 1, 2 >= 2, 5 > 3, 5 > 4
- new_listToMaybe17(wz304, Succ(wz3050), Succ(wz3060), wz307, wz308, wz309) → new_listToMaybe17(wz304, wz3050, wz3060, wz307, wz308, wz309)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe17(wz272, wz27500, wz27600, wz277, wz27500, wz278)
The graph contains the following edges 1 >= 1, 4 > 2, 5 > 3, 6 >= 4, 4 > 5, 7 >= 6
- new_listToMaybe13(wz170, wz168, :%(Neg(Zero), wz17101), wz1711, wz188, wz187) → new_listToMaybe14(wz187, wz168, wz17101, wz170, wz1711, wz187)
The graph contains the following edges 6 >= 1, 2 >= 2, 3 > 3, 1 >= 4, 4 >= 5, 6 >= 6
- new_listToMaybe13(wz170, wz168, :%(Pos(wz171000), wz17101), wz1711, wz188, wz187) → new_listToMaybe14(wz187, wz168, wz17101, wz170, wz1711, wz187)
The graph contains the following edges 6 >= 1, 2 >= 2, 3 > 3, 1 >= 4, 4 >= 5, 6 >= 6
- new_listToMaybe15(wz272, Succ(wz2730), Zero, wz275, wz276, wz277, wz278) → new_listToMaybe14(wz272, wz275, wz276, wz277, wz278, wz272)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4, 7 >= 5, 1 >= 6
- new_listToMaybe15(wz272, Zero, Succ(wz2740), wz275, wz276, wz277, wz278) → new_listToMaybe14(wz272, wz275, wz276, wz277, wz278, wz272)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4, 7 >= 5, 1 >= 6
- new_listToMaybe17(wz304, Zero, Succ(wz3060), wz307, wz308, wz309) → new_listToMaybe16(wz304, wz307, Pos(Succ(wz308)), wz309, wz304)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4, 1 >= 5
- new_listToMaybe17(wz304, Succ(wz3050), Zero, wz307, wz308, wz309) → new_listToMaybe16(wz304, wz307, Pos(Succ(wz308)), wz309, wz304)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4, 1 >= 5
- new_listToMaybe18(wz311, Zero, Succ(wz3130), wz314, wz315, wz316) → new_listToMaybe16(wz311, wz314, Neg(Succ(wz315)), wz316, wz311)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4, 1 >= 5
- new_listToMaybe18(wz311, Succ(wz3120), Zero, wz314, wz315, wz316) → new_listToMaybe16(wz311, wz314, Neg(Succ(wz315)), wz316, wz311)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Pos(Zero), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Zero), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Pos(Zero), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Zero), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Pos(Zero), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Succ(wz27500)), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Neg(Zero), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Zero), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Neg(Zero), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Zero), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Neg(wz2760), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Succ(wz27500)), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Neg(Zero), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Succ(wz27500)), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
- new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Pos(wz2760), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Succ(wz27500)), wz278, wz272)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4, 1 >= 5
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe19(wz31, :%(Neg(Zero), wz411101), wz41111, wz135, wz134) → new_listToMaybe24(wz134, wz31, wz411101, wz41111)
new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe22(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe24(wz134, Neg(Zero), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Zero)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe23(wz134, wz31, wz411101, wz41111) → new_listToMaybe20(wz134, wz31, wz41111, wz134)
new_listToMaybe20(wz116, wz31, :(wz41110, wz41111), wz117) → new_listToMaybe19(wz31, wz41110, wz41111, new_primPlusNat(wz117), new_primPlusNat(wz117))
new_listToMaybe19(wz31, :%(Pos(Succ(wz41110000)), wz411101), wz41111, wz135, wz134) → new_listToMaybe20(wz134, wz31, wz41111, wz134)
new_listToMaybe24(wz134, Neg(Succ(wz3100)), Neg(Zero), wz41111) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Zero)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe21(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Neg(wz4111010)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe24(wz134, Neg(Succ(wz3100)), Pos(wz4111010), wz41111) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Pos(Zero), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe24(wz134, Pos(Succ(wz3100)), Neg(wz4111010), wz41111) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Neg(Zero), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
new_listToMaybe19(Neg(Zero), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
new_listToMaybe19(Pos(Zero), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe21(wz230, Zero, Succ(wz2320), wz233, wz234) → new_listToMaybe20(wz230, Pos(Succ(wz233)), wz234, wz230)
new_listToMaybe21(wz230, Succ(wz2310), Zero, wz233, wz234) → new_listToMaybe20(wz230, Pos(Succ(wz233)), wz234, wz230)
new_listToMaybe24(wz134, Pos(Succ(wz3100)), Pos(Zero), wz41111) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe24(wz134, Pos(Zero), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe22(wz236, Zero, Succ(wz2380), wz239, wz240) → new_listToMaybe20(wz236, Neg(Succ(wz239)), wz240, wz236)
new_listToMaybe22(wz236, Succ(wz2370), Zero, wz239, wz240) → new_listToMaybe20(wz236, Neg(Succ(wz239)), wz240, wz236)
new_listToMaybe19(wz31, :%(Neg(Succ(wz41110000)), wz411101), wz41111, wz135, wz134) → new_listToMaybe23(wz134, wz31, wz411101, wz41111)
new_listToMaybe24(wz134, Pos(Zero), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Pos(wz4111010)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe21(wz230, Succ(wz2310), Succ(wz2320), wz233, wz234) → new_listToMaybe21(wz230, wz2310, wz2320, wz233, wz234)
new_listToMaybe22(wz236, Succ(wz2370), Succ(wz2380), wz239, wz240) → new_listToMaybe22(wz236, wz2370, wz2380, wz239, wz240)
new_listToMaybe24(wz134, Neg(Succ(wz3100)), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe22(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe24(wz134, Pos(Succ(wz3100)), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe21(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe24(wz134, Neg(Zero), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
The TRS R consists of the following rules:
new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_listToMaybe20(wz116, wz31, :(wz41110, wz41111), wz117) → new_listToMaybe19(wz31, wz41110, wz41111, new_primPlusNat(wz117), new_primPlusNat(wz117))
The graph contains the following edges 2 >= 1, 3 > 2, 3 > 3
- new_listToMaybe19(wz31, :%(Neg(Zero), wz411101), wz41111, wz135, wz134) → new_listToMaybe24(wz134, wz31, wz411101, wz41111)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 3 >= 4
- new_listToMaybe19(wz31, :%(Neg(Succ(wz41110000)), wz411101), wz41111, wz135, wz134) → new_listToMaybe23(wz134, wz31, wz411101, wz41111)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 3, 3 >= 4
- new_listToMaybe22(wz236, Succ(wz2370), Succ(wz2380), wz239, wz240) → new_listToMaybe22(wz236, wz2370, wz2380, wz239, wz240)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5
- new_listToMaybe21(wz230, Succ(wz2310), Succ(wz2320), wz233, wz234) → new_listToMaybe21(wz230, wz2310, wz2320, wz233, wz234)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5
- new_listToMaybe23(wz134, wz31, wz411101, wz41111) → new_listToMaybe20(wz134, wz31, wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Pos(Succ(wz3100)), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe21(wz134, wz3100, wz41110100, wz3100, wz41111)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 2 > 4, 4 >= 5
- new_listToMaybe24(wz134, Neg(Succ(wz3100)), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe22(wz134, wz3100, wz41110100, wz3100, wz41111)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 2 > 4, 4 >= 5
- new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe21(wz134, wz3100, wz41110100, wz3100, wz41111)
The graph contains the following edges 5 >= 1, 1 > 2, 2 > 3, 1 > 4, 3 >= 5
- new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe22(wz134, wz3100, wz41110100, wz3100, wz41111)
The graph contains the following edges 5 >= 1, 1 > 2, 2 > 3, 1 > 4, 3 >= 5
- new_listToMaybe24(wz134, Neg(Zero), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Neg(Succ(wz3100)), Neg(Zero), wz41111) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Neg(Succ(wz3100)), Pos(wz4111010), wz41111) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Pos(Succ(wz3100)), Neg(wz4111010), wz41111) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Pos(Succ(wz3100)), Pos(Zero), wz41111) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Pos(Zero), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Pos(Zero), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe24(wz134, Neg(Zero), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 1 >= 4
- new_listToMaybe22(wz236, Zero, Succ(wz2380), wz239, wz240) → new_listToMaybe20(wz236, Neg(Succ(wz239)), wz240, wz236)
The graph contains the following edges 1 >= 1, 5 >= 3, 1 >= 4
- new_listToMaybe22(wz236, Succ(wz2370), Zero, wz239, wz240) → new_listToMaybe20(wz236, Neg(Succ(wz239)), wz240, wz236)
The graph contains the following edges 1 >= 1, 5 >= 3, 1 >= 4
- new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Zero)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(wz31, :%(Pos(Succ(wz41110000)), wz411101), wz41111, wz135, wz134) → new_listToMaybe20(wz134, wz31, wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Zero)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Neg(wz4111010)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Pos(Zero), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Neg(Zero), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Neg(Zero), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Pos(Zero), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 2 > 2, 3 >= 3, 5 >= 4
- new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Pos(wz4111010)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
The graph contains the following edges 5 >= 1, 1 >= 2, 3 >= 3, 5 >= 4
- new_listToMaybe21(wz230, Zero, Succ(wz2320), wz233, wz234) → new_listToMaybe20(wz230, Pos(Succ(wz233)), wz234, wz230)
The graph contains the following edges 1 >= 1, 5 >= 3, 1 >= 4
- new_listToMaybe21(wz230, Succ(wz2310), Zero, wz233, wz234) → new_listToMaybe20(wz230, Pos(Succ(wz233)), wz234, wz230)
The graph contains the following edges 1 >= 1, 5 >= 3, 1 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe25(wz202, Zero, Zero, Neg(Zero), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Zero), wz208)
new_listToMaybe26(wz130, wz31, wz411101, wz3000, :(wz411110, wz411111)) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Neg(Zero), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Succ(wz20500)), wz208)
new_listToMaybe31(wz3000, wz31, :%(Neg(wz4111000), wz411101), :(wz411110, wz411111), wz131, wz130) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
new_listToMaybe25(wz202, Zero, Zero, Pos(Zero), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Zero), wz208)
new_listToMaybe27(wz280, Zero, Succ(wz2820), wz283, wz284, wz285) → new_listToMaybe28(wz280, wz283, Pos(Succ(wz284)), wz285)
new_listToMaybe27(wz280, Succ(wz2810), Zero, wz283, wz284, wz285) → new_listToMaybe28(wz280, wz283, Pos(Succ(wz284)), wz285)
new_listToMaybe27(wz280, Succ(wz2810), Succ(wz2820), wz283, wz284, wz285) → new_listToMaybe27(wz280, wz2810, wz2820, wz283, wz284, wz285)
new_listToMaybe28(wz130, wz3000, wz31, :(wz411110, wz411111)) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
new_listToMaybe25(wz202, Zero, Zero, Neg(Zero), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Zero), wz208)
new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe27(wz202, wz20500, wz20600, wz207, wz20500, wz208)
new_listToMaybe25(wz202, Succ(wz2030), Succ(wz2040), wz205, wz206, wz207, wz208) → new_listToMaybe25(wz202, wz2030, wz2040, wz205, wz206, wz207, wz208)
new_listToMaybe29(wz287, Succ(wz2880), Zero, wz290, wz291, wz292) → new_listToMaybe28(wz287, wz290, Neg(Succ(wz291)), wz292)
new_listToMaybe29(wz287, Zero, Succ(wz2890), wz290, wz291, wz292) → new_listToMaybe28(wz287, wz290, Neg(Succ(wz291)), wz292)
new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Pos(Zero), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Succ(wz20500)), wz208)
new_listToMaybe25(wz202, Zero, Succ(wz2040), wz205, wz206, wz207, wz208) → new_listToMaybe26(wz202, wz205, wz206, wz207, wz208)
new_listToMaybe25(wz202, Succ(wz2030), Zero, wz205, wz206, wz207, wz208) → new_listToMaybe26(wz202, wz205, wz206, wz207, wz208)
new_listToMaybe25(wz202, Zero, Zero, Pos(Zero), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Zero), wz208)
new_listToMaybe31(wz3000, wz31, :%(Pos(Zero), wz411101), wz41111, wz131, wz130) → new_listToMaybe26(wz130, wz31, wz411101, wz3000, wz41111)
new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Neg(wz2060), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Succ(wz20500)), wz208)
new_listToMaybe30(wz3000, wz31, wz41110, wz41111, wz120, wz121) → new_listToMaybe31(wz3000, wz31, wz41110, wz41111, new_primPlusNat(wz120), new_primPlusNat(wz120))
new_listToMaybe31(wz3000, wz31, :%(Pos(Succ(wz41110000)), wz411101), wz41111, wz131, wz130) → new_listToMaybe25(wz130, wz3000, wz41110000, wz31, wz411101, wz3000, wz41111)
new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe29(wz202, wz20500, wz20600, wz207, wz20500, wz208)
new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Pos(wz2060), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Succ(wz20500)), wz208)
new_listToMaybe29(wz287, Succ(wz2880), Succ(wz2890), wz290, wz291, wz292) → new_listToMaybe29(wz287, wz2880, wz2890, wz290, wz291, wz292)
The TRS R consists of the following rules:
new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_listToMaybe28(wz130, wz3000, wz31, :(wz411110, wz411111)) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
The graph contains the following edges 2 >= 1, 3 >= 2, 4 > 3, 4 > 4, 1 >= 5, 1 >= 6
- new_listToMaybe30(wz3000, wz31, wz41110, wz41111, wz120, wz121) → new_listToMaybe31(wz3000, wz31, wz41110, wz41111, new_primPlusNat(wz120), new_primPlusNat(wz120))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
- new_listToMaybe27(wz280, Succ(wz2810), Succ(wz2820), wz283, wz284, wz285) → new_listToMaybe27(wz280, wz2810, wz2820, wz283, wz284, wz285)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe27(wz202, wz20500, wz20600, wz207, wz20500, wz208)
The graph contains the following edges 1 >= 1, 4 > 2, 5 > 3, 6 >= 4, 4 > 5, 7 >= 6
- new_listToMaybe25(wz202, Succ(wz2030), Succ(wz2040), wz205, wz206, wz207, wz208) → new_listToMaybe25(wz202, wz2030, wz2040, wz205, wz206, wz207, wz208)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
- new_listToMaybe31(wz3000, wz31, :%(Pos(Succ(wz41110000)), wz411101), wz41111, wz131, wz130) → new_listToMaybe25(wz130, wz3000, wz41110000, wz31, wz411101, wz3000, wz41111)
The graph contains the following edges 6 >= 1, 1 >= 2, 3 > 3, 2 >= 4, 3 > 5, 1 >= 6, 4 >= 7
- new_listToMaybe31(wz3000, wz31, :%(Pos(Zero), wz411101), wz41111, wz131, wz130) → new_listToMaybe26(wz130, wz31, wz411101, wz3000, wz41111)
The graph contains the following edges 6 >= 1, 2 >= 2, 3 > 3, 1 >= 4, 4 >= 5
- new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe29(wz202, wz20500, wz20600, wz207, wz20500, wz208)
The graph contains the following edges 1 >= 1, 4 > 2, 5 > 3, 6 >= 4, 4 > 5, 7 >= 6
- new_listToMaybe29(wz287, Succ(wz2880), Succ(wz2890), wz290, wz291, wz292) → new_listToMaybe29(wz287, wz2880, wz2890, wz290, wz291, wz292)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_listToMaybe26(wz130, wz31, wz411101, wz3000, :(wz411110, wz411111)) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
The graph contains the following edges 4 >= 1, 2 >= 2, 5 > 3, 5 > 4, 1 >= 5, 1 >= 6
- new_listToMaybe31(wz3000, wz31, :%(Neg(wz4111000), wz411101), :(wz411110, wz411111), wz131, wz130) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4, 6 >= 5, 6 >= 6
- new_listToMaybe25(wz202, Zero, Succ(wz2040), wz205, wz206, wz207, wz208) → new_listToMaybe26(wz202, wz205, wz206, wz207, wz208)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4, 7 >= 5
- new_listToMaybe25(wz202, Succ(wz2030), Zero, wz205, wz206, wz207, wz208) → new_listToMaybe26(wz202, wz205, wz206, wz207, wz208)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4, 7 >= 5
- new_listToMaybe27(wz280, Succ(wz2810), Zero, wz283, wz284, wz285) → new_listToMaybe28(wz280, wz283, Pos(Succ(wz284)), wz285)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4
- new_listToMaybe27(wz280, Zero, Succ(wz2820), wz283, wz284, wz285) → new_listToMaybe28(wz280, wz283, Pos(Succ(wz284)), wz285)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Neg(Zero), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Zero), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Neg(Zero), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Succ(wz20500)), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Pos(Zero), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Zero), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Neg(Zero), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Zero), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Pos(Zero), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Succ(wz20500)), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Pos(Zero), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Zero), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Neg(wz2060), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Succ(wz20500)), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Pos(wz2060), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Succ(wz20500)), wz208)
The graph contains the following edges 1 >= 1, 6 >= 2, 4 >= 3, 7 >= 4
- new_listToMaybe29(wz287, Succ(wz2880), Zero, wz290, wz291, wz292) → new_listToMaybe28(wz287, wz290, Neg(Succ(wz291)), wz292)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4
- new_listToMaybe29(wz287, Zero, Succ(wz2890), wz290, wz291, wz292) → new_listToMaybe28(wz287, wz290, Neg(Succ(wz291)), wz292)
The graph contains the following edges 1 >= 1, 4 >= 2, 6 >= 4